These example models can also be found in the Verics distribution:

• A faulty train controller: source FTC.vxs, ISPL output FTC.ispl.
• A controller just as faulty, but using protocols: source FTCp.vxs, ISPL output FTCp.ispl.
• A simple pipeline: source pipeline.vxs, ISPL output pipeline.ispl.
• Dining cryptographers, a more preprocessor-intensive version for any number of seats: source dcN.vxs, ISPL output dcN.ispl.
• The model of energy network: Microgrid.java: source of the model, Microgrid.pctl: properties to compute, Microgrid.nm: the resulting Prism file.
• An image acquisition system, source: Camera.java, Bus.java, VideoProcessing.java, ImageAcquisitionSystem.java, PTAs for Prism: ImageAcquisitionSystem.nm, architecture: ImageAcquisitionSystem.aadl.

Command line:

• veric -oi FTC.vxs
• veric -oi FTCp.vxs
• veric -oi pipeline.vxs
• veric -oi dcN.vxs
• verics Microgrid.java --const HOUSEHOLDS=3~9:2 -op -v0 -sh -i
• prism Microgrid.nm Microgrid.pctl
• verics -U -v0 -op -sh -i -Da Camera.java VideoProcessing.java ImageAcquisitionSystem.java